YES 16.346 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((minimum :: [Float ->  Float) :: [Float ->  Float)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((minimum :: [Float ->  Float) :: [Float ->  Float)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
min x y
 | x <= y
 = x
 | otherwise
 = y

is transformed to
min x y = min2 x y

min1 x y True = x
min1 x y False = min0 x y otherwise

min0 x y True = y

min2 x y = min1 x y (x <= y)

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (minimum :: [Float ->  Float)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vx4400), Succ(vx3100000)) → new_primPlusNat(vx4400, vx3100000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vx300000), vx310000) → new_primMulNat(vx300000, vx310000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat0(Succ(vx2000), Succ(vx2200)) → new_primMulNat0(vx2000, Succ(vx2200))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_not(Succ(vx37800), Succ(vx40700)) → new_not(vx37800, vx40700)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldl(vx30, :(vx310, vx311)) → new_foldl(new_min1(vx30, vx310), vx311)

The TRS R consists of the following rules:

new_min167(vx19, vx2000, vx21, vx2200, True) → Float(Pos(Succ(vx19)), Pos(Succ(vx2000)))
new_min1108(vx310000, vx310100, False) → new_min01(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), vx310000, vx310100)
new_min1155(vx310000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Zero)))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Pos(Succ(vx30000)), Pos(Succ(vx30100))))
new_min153(vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min144(vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min193(vx3010000, vx310000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min00(vx14, vx150, vx16, vx170) → Float(Pos(Succ(vx16)), Pos(vx170))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min1132(vx30000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min12(vx14, vx1500, vx16, False) → Float(Pos(Succ(vx16)), Pos(Zero))
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min124(vx30000, vx310100, new_not2(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Pos(Zero), Pos(Zero))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Pos(Zero), Pos(Zero))
new_min118(vx30000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min1133(vx3010000, vx310000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1147(vx310000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min159(vx3010000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min184(vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_min129(vx310100, True) → Float(Neg(Zero), Pos(Succ(Zero)))
new_min186(vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_min119(vx35, Pos(vx360), vx37, Pos(vx380), Succ(vx3780)) → new_min120(vx35, vx360, vx37, vx380, new_not4(vx3780, new_primMulNat1(vx360, vx380)))
new_min1149(vx3010000, vx310000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min155(vx310100, new_not9(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Pos(Zero), Neg(Zero))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min158(vx3010000, vx310000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Neg(Zero), Pos(Zero))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min1108(vx310000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min119(vx35, Pos(vx360), vx37, Pos(vx380), Zero) → new_min120(vx35, vx360, vx37, vx380, new_not2(new_primMulNat1(vx360, vx380)))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min1143(vx30000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min10(vx14, Neg(Zero), vx16, Pos(Zero), Zero) → new_min116(vx14, vx16, new_not3(Zero))
new_min1162(vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min174(vx3010000, Float(Pos(Succ(vx310000)), Neg(Succ(vx310100))), new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min148(vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min1111(vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1127(vx19, Neg(Succ(vx2000)), vx21, Pos(Zero), Zero) → new_min165(vx19, vx2000, vx21, new_not9(Zero))
new_min10(vx14, Pos(Succ(vx1500)), vx16, Pos(Zero), Succ(vx450)) → new_min12(vx14, vx1500, vx16, new_not1(vx450))
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min144(vx310100, new_not3(new_primPlusNat0(Zero, Succ(vx310100))))
new_not0(Zero, Zero) → new_not10
new_min194(vx310100, True) → Float(Pos(Zero), Pos(Succ(Zero)))
new_min1161(vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_min193(vx3010000, vx310000, vx310100, False) → new_min01(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), vx310000, vx310100)
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min187(vx310000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Neg(Zero), Neg(Zero))
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min181(vx310100, new_not2(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Neg(Zero))
new_min1128(vx30000, vx3010000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min1116(vx30000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min1143(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min152(vx30000, vx3010000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min173(vx310000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Zero)))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(vx301000)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min1137(vx301000, Float(Neg(Zero), Neg(Succ(vx310100))), vx310100)
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min1164(vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min1154(vx30000, vx310100, new_not3(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Neg(Zero), Neg(Zero))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Neg(Zero), Neg(Zero))
new_min1115(vx30000, vx3010000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min129(vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min140(vx3010000, vx310000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1154(vx30000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Neg(Zero))) → new_min168(vx30000, new_not11(Zero))
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min198(vx30000, vx3010000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1145(vx310000, vx310100, False) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_min197(vx11, True) → Float(Pos(Zero), Neg(Succ(Succ(Zero))))
new_min10(vx14, Pos(Zero), vx16, Pos(Zero), Zero) → new_min14(vx14, vx16, new_not2(Zero))
new_min1150(vx310000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min1148(vx310000, vx310100, new_not9(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min132(vx310100, new_not3(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min1105(vx30000, vx3010000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min189(vx30000, vx310100, new_not11(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min178(vx310100, new_not2(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min1136(vx310000, vx310100, new_not9(new_primPlusNat0(Zero, Succ(vx310100))))
new_min189(vx30000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min1129(vx30000, vx3010000, vx310100, True) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_min199(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_min138(vx310000, vx310100, True) → Float(Pos(Zero), Neg(Succ(Zero)))
new_min1133(vx3010000, vx310000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1167(vx19, vx21, vx2200, False) → Float(Neg(Succ(vx21)), Neg(Succ(vx2200)))
new_min10(vx14, Neg(Zero), vx16, Neg(Succ(vx1700)), Zero) → new_min17(vx14, vx16, vx1700, new_not2(Zero))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min128(vx310000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1127(vx19, Pos(Zero), vx21, Neg(Zero), Succ(vx1410)) → new_min1165(vx19, vx21, new_not7(Zero, vx1410))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min1119(vx30000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min122(vx35, vx360, vx37, vx380, True) → Float(Neg(Succ(vx35)), Neg(vx360))
new_min1152(vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_min17(vx14, vx16, vx1700, True) → Float(Pos(Succ(vx14)), Neg(Zero))
new_min1109(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Neg(Succ(Zero)))
new_min1139(vx3010000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min10(vx14, Pos(Succ(vx1500)), vx16, Neg(Succ(vx1700)), Zero) → new_min19(vx14, vx1500, vx16, vx1700, new_not3(new_primPlusNat0(new_primMulNat1(vx1500, Succ(vx1700)), Succ(vx1700))))
new_primMulNat2(Succ(vx300000), vx310000) → new_primPlusNat1(new_primMulNat2(vx300000, vx310000), vx310000)
new_min1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Pos(Zero), Pos(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Pos(Succ(vx30000)), Pos(Zero))
new_min1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Pos(Zero), Pos(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Pos(Succ(vx30000)), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min140(vx3010000, vx310000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min198(vx30000, vx3010000, vx310100, True) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_min10(vx14, Neg(vx150), vx16, Pos(vx170), Succ(vx450)) → new_min00(vx14, vx150, vx16, vx170)
new_min1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Neg(Succ(vx30000)), Neg(Zero)))
new_min1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Neg(Zero), Neg(Succ(vx30100))))
new_min1170(vx19, vx200, vx21, vx220, True) → Float(Pos(Succ(vx19)), Neg(vx200))
new_min169(vx30000, vx3010000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min1109(vx30000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min160(vx310100, new_not11(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1123(vx310000, vx310100, True) → Float(Pos(Zero), Neg(Succ(Zero)))
new_not3(Zero) → new_not10
new_min133(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_min177(vx30000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min113(vx14, vx1500, vx16, vx1700, False) → new_min00(vx14, Succ(vx1500), vx16, Succ(vx1700))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min126(vx30000, vx3010000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min132(vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min182(vx3010000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1102(vx310000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Zero)))
new_min1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Pos(Succ(vx30000)), Pos(Zero)))
new_min1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Pos(Zero), Pos(Succ(vx30100))))
new_min16(vx14, vx1500, vx16, True) → Float(Pos(Succ(vx14)), Neg(Succ(vx1500)))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1150(vx310000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1140(vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min147(vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min164(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_min127(vx310100, True) → Float(Neg(Zero), Pos(Succ(Zero)))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min133(vx30000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min110(vx14, vx1500, vx16, False) → new_min0(vx14, Succ(vx1500), vx16, Zero)
new_min19(vx14, vx1500, vx16, vx1700, False) → new_min0(vx14, Succ(vx1500), vx16, Succ(vx1700))
new_not9(Succ(vx1610)) → new_not1(vx1610)
new_min10(vx14, Pos(Succ(vx1500)), vx16, Pos(Succ(vx1700)), Zero) → new_min11(vx14, vx1500, vx16, vx1700, new_not2(new_primPlusNat0(new_primMulNat1(vx1500, Succ(vx1700)), Succ(vx1700))))
new_min1141(vx30, Neg(vx310), vx32, Pos(vx330), Zero) → new_min145(vx30, vx310, vx32, vx330, new_not9(new_primMulNat1(vx310, vx330)))
new_min114(vx14, vx1500, vx16, True) → Float(Pos(Succ(vx14)), Neg(Succ(vx1500)))
new_min1136(vx310000, vx310100, True) → Float(Pos(Zero), Neg(Succ(Zero)))
new_min1141(vx30, Neg(vx310), vx32, Neg(vx330), Zero) → new_min143(vx30, vx310, vx32, vx330, new_not11(new_primMulNat1(vx310, vx330)))
new_min1134(vx3010000, vx310000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1156(vx310000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min127(vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min1101(vx30000, vx3010000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min176(vx30, vx310, vx32, vx330, True) → Float(Neg(Succ(vx30)), Pos(vx310))
new_min1159(vx3010000, vx310000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_min1148(vx310000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Zero)))
new_not2(Zero) → new_not10
new_min1167(vx19, vx21, vx2200, True) → Float(Pos(Succ(vx19)), Pos(Zero))
new_min141(vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Pos(Zero), Pos(Zero)))
new_min121(vx35, vx360, vx37, vx380, False) → Float(Neg(Succ(vx37)), Neg(vx380))
new_min1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Neg(Succ(vx30000)), Neg(Zero))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Neg(Zero), Neg(Zero))
new_min1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Neg(Zero), Neg(Succ(vx30100)))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Neg(Zero), Neg(Zero))
new_min1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Succ(vx30000)), Neg(Zero))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Neg(Zero), Neg(Zero))
new_min1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Neg(Succ(vx30100)))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Neg(Zero), Neg(Zero))
new_min14(vx14, vx16, True) → Float(Pos(Succ(vx14)), Pos(Zero))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1122(vx3010000, vx310000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Neg(Zero), Neg(Zero))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Neg(Zero), Neg(Zero))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min197(Float(Pos(Zero), Pos(Succ(vx310100))), new_not3(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1151(vx3010000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_min191(vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min182(vx3010000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min139(vx3010000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min1160(vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_min143(vx30, vx310, vx32, vx330, False) → Float(Pos(Succ(vx32)), Neg(vx330))
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min185(vx30000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min195(vx30000, vx310100, new_not9(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Neg(Succ(vx30000)), Neg(Zero))
new_min1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Neg(Zero), Neg(Succ(vx30100)))
new_min1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Neg(Succ(vx30000)), Neg(Zero))
new_min1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Neg(Zero), Neg(Succ(vx30100)))
new_min165(vx19, vx2000, vx21, False) → Float(Neg(Succ(vx21)), Pos(Zero))
new_min116(vx14, vx16, True) → Float(Pos(Succ(vx14)), Neg(Zero))
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min1126(vx310100, new_not2(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1103(vx3010000, vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_min1127(vx19, Pos(Succ(vx2000)), vx21, Neg(Zero), Zero) → new_min125(vx19, vx2000, vx21, new_not9(Zero))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Pos(Zero), Pos(Zero))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Pos(Zero), Pos(Zero))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Pos(Zero), Pos(Zero))
new_primMulNat1(Zero, Zero) → Zero
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min130(vx30000, vx310100, new_not9(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min1109(vx30000, vx310100, new_not2(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1162(vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min125(vx19, vx2000, vx21, True) → Float(Pos(Succ(vx19)), Pos(Succ(vx2000)))
new_min155(vx310100, True) → Float(Neg(Zero), Neg(Succ(Zero)))
new_min1141(vx30, Pos(vx310), vx32, Pos(vx330), Succ(vx2540)) → new_min176(vx30, vx310, vx32, vx330, new_not13(vx2540, vx310, vx330))
new_min1104(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Pos(Succ(Zero)))
new_min178(vx310100, True) → Float(Pos(Zero), Pos(Succ(Zero)))
new_min186(vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min123(vx35, vx360, vx37, vx380, True) → Float(Neg(Succ(vx35)), Neg(vx360))
new_min135(vx310000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Zero)))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Neg(Zero), Neg(Zero))
new_min10(vx14, Neg(Succ(vx1500)), vx16, Neg(Zero), Succ(vx450)) → new_min16(vx14, vx1500, vx16, new_not1(vx450))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min197(Float(Pos(Zero), Neg(Succ(vx310100))), new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min153(vx310100, True) → Float(Neg(Zero), Neg(Succ(Zero)))
new_min1159(vx3010000, vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_min1112(vx30000, vx3010000, vx310100, True) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_min1107(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Neg(Succ(Zero)))
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min1104(vx30000, vx310100, new_not11(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1107(vx30000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min1127(vx19, Neg(Zero), vx21, Pos(Zero), Succ(vx1410)) → new_min1169(vx19, vx21, new_not7(Zero, vx1410))
new_min1104(vx30000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min168(vx5, True) → Float(Pos(Succ(vx5)), Neg(Zero))
new_min1156(vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_min144(vx310100, True) → Float(Pos(Zero), Neg(Succ(Zero)))
new_min198(vx30000, vx3010000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1159(vx3010000, vx310000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min151(vx3010000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min14(vx14, vx16, False) → Float(Pos(Succ(vx16)), Pos(Zero))
new_min1106(vx19, vx200, vx21, vx220, False) → Float(Neg(Succ(vx21)), Pos(vx220))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min1114(vx30000, vx310100, new_not2(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1112(vx30000, vx3010000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min1127(vx19, Neg(Zero), vx21, Pos(Succ(vx2200)), Zero) → new_min1168(vx19, vx21, vx2200, new_not9(Zero))
new_min1125(vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min134(vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min1119(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_min15(vx14, vx1500, vx16, vx1700, True) → Float(Pos(Succ(vx14)), Neg(Succ(vx1500)))
new_min191(vx310100, True) → Float(Neg(Zero), Pos(Succ(Zero)))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1103(vx3010000, vx310000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1127(vx19, Neg(Succ(vx2000)), vx21, Pos(Zero), Succ(vx1410)) → new_min165(vx19, vx2000, vx21, new_not7(Zero, vx1410))
new_not7(Zero, vx1410) → new_not12
new_min1141(vx30, Neg(vx310), vx32, Neg(vx330), Succ(vx2540)) → new_min143(vx30, vx310, vx32, vx330, new_not13(vx2540, vx310, vx330))
new_min10(vx14, Pos(Zero), vx16, Pos(Succ(vx1700)), Zero) → new_min13(vx14, vx16, vx1700, new_not2(Zero))
new_min195(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Neg(Succ(Zero)))
new_min126(vx30000, vx3010000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Neg(Succ(vx30000)), Neg(Zero))
new_min1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Neg(Zero), Neg(Succ(vx30100)))
new_min1121(vx310000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Zero)))
new_min162(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min1115(vx30000, vx3010000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min158(vx3010000, vx310000, vx310100, False) → new_min01(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), vx310000, vx310100)
new_min1127(vx19, Neg(Succ(vx2000)), vx21, Pos(Succ(vx2200)), Succ(vx1410)) → new_min196(vx19, vx2000, vx21, vx2200, new_not7(new_primPlusNat0(new_primMulNat1(vx2000, Succ(vx2200)), Succ(vx2200)), vx1410))
new_min124(vx30000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min124(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Pos(Succ(Zero)))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min1117(vx30000, vx3010000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min154(vx3010000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min10(vx14, Pos(Zero), vx16, Neg(Succ(vx1700)), Zero) → new_min111(vx14, vx16, vx1700, new_not3(Zero))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Neg(Zero), Neg(Zero))
new_min1137(Zero, vx11, vx12) → new_min197(vx11, new_not11(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx12)), Succ(vx12))))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min1128(vx30000, vx3010000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min170(vx310000, vx310100, False) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_min160(vx310100, True) → Float(Pos(Zero), Neg(Succ(Zero)))
new_min1116(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min1113(vx30000, vx3010000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1100(vx310000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Zero)))
new_not4(vx3780, Succ(vx4070)) → new_not0(vx3780, vx4070)
new_min1(Float(Neg(Succ(vx30000)), vx301), Float(Neg(Succ(vx310000)), vx3101)) → new_min119(vx30000, vx301, vx310000, vx3101, new_primPlusNat0(new_primMulNat1(vx30000, Succ(vx310000)), Succ(vx310000)))
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min188(vx30000, vx3010000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min10(vx14, Neg(Zero), vx16, Neg(Zero), Zero) → new_min18(vx14, vx16, new_not2(Zero))
new_min132(vx310100, True) → Float(Pos(Zero), Pos(Succ(Zero)))
new_min1164(vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_min1161(vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min10(vx14, Pos(Zero), vx16, Neg(Zero), Zero) → new_min112(vx14, vx16, new_not3(Zero))
new_min1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Pos(Zero), Pos(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Pos(Succ(vx30000)), Pos(Zero))
new_min1138(vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_min116(vx14, vx16, False) → new_min00(vx14, Zero, vx16, Zero)
new_min1123(vx310000, vx310100, False) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_min1152(vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min111(vx14, vx16, vx1700, True) → Float(Pos(Succ(vx14)), Pos(Zero))
new_min1102(vx310000, vx310100, False) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_min140(vx3010000, vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_min13(vx14, vx16, vx1700, False) → new_min01(Float(Pos(Succ(vx14)), Pos(Zero)), vx16, vx1700)
new_not2(Succ(vx3920)) → new_not7(Zero, vx3920)
new_min130(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Pos(Succ(Zero)))
new_min181(vx310100, True) → Float(Neg(Zero), Pos(Succ(Zero)))
new_min16(vx14, vx1500, vx16, False) → Float(Pos(Succ(vx16)), Neg(Zero))
new_min190(vx30000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min1112(vx30000, vx3010000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Succ(vx30000)), Pos(Zero))
new_min10(vx14, Pos(vx150), vx16, Neg(vx170), Succ(vx450)) → new_min0(vx14, vx150, vx16, vx170)
new_min112(vx14, vx16, True) → Float(Pos(Succ(vx14)), Pos(Zero))
new_min1127(vx19, Neg(Succ(vx2000)), vx21, Pos(Succ(vx2200)), Zero) → new_min196(vx19, vx2000, vx21, vx2200, new_not9(new_primPlusNat0(new_primMulNat1(vx2000, Succ(vx2200)), Succ(vx2200))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min1152(vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min188(vx30000, vx3010000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min1142(vx30000, vx3010000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min192(vx30000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_not9(Zero) → new_not10
new_primPlusNat1(Zero, vx310000) → Succ(vx310000)
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min1121(vx310000, vx310100, new_not2(new_primPlusNat0(Zero, Succ(vx310100))))
new_min119(vx35, Neg(vx360), vx37, Pos(vx380), Succ(vx3780)) → new_min122(vx35, vx360, vx37, vx380, new_not5(vx3780, new_primMulNat1(vx360, vx380)))
new_min1100(vx310000, vx310100, False) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_min166(vx3010000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1135(vx310000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min12(vx14, vx1500, vx16, True) → Float(Pos(Succ(vx14)), Pos(Succ(vx1500)))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min177(vx30000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1168(vx19, vx21, vx2200, False) → Float(Neg(Succ(vx21)), Pos(Succ(vx2200)))
new_min1163(vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min190(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Pos(Succ(Zero)))
new_min01(vx563, vx564, vx565) → Float(Pos(Succ(vx564)), Pos(Succ(vx565)))
new_not12new_not14
new_min171(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Pos(Succ(Zero)))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min186(vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min189(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Neg(Succ(Zero)))
new_min1137(Succ(vx100), vx11, vx12) → new_min174(vx100, vx11, new_not11(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx100, Succ(vx12)), Succ(vx12)), Succ(vx12)), Succ(vx12))))
new_min1150(vx310000, vx310100, False) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_min141(vx310000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Zero)))
new_min161(vx310000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Zero)))
new_min113(vx14, vx1500, vx16, vx1700, True) → Float(Pos(Succ(vx14)), Neg(Succ(vx1500)))
new_min1169(vx19, vx21, True) → Float(Pos(Succ(vx19)), Neg(Zero))
new_min117(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Pos(Succ(Zero)))
new_min172(vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_min174(vx100, vx11, True) → Float(Pos(Zero), Neg(Succ(Succ(Succ(vx100)))))
new_min1105(vx30000, vx3010000, vx310100, True) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_min173(vx310000, vx310100, False) → new_min01(Float(Neg(Zero), Pos(Succ(Zero))), vx310000, vx310100)
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min171(vx30000, vx310100, new_not3(new_primPlusNat0(Zero, Succ(vx310100))))
new_min180(vx3010000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min1153(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_min1115(vx30000, vx3010000, vx310100, True) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min150(vx30000, vx310100, new_not11(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min1162(vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min196(vx19, vx2000, vx21, vx2200, True) → Float(Pos(Succ(vx19)), Neg(Succ(vx2000)))
new_min1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Pos(Zero), Neg(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Pos(Succ(vx30000)), Neg(Zero))
new_min1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Neg(Succ(vx30000)), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Neg(Zero), Pos(Succ(vx30100)))
new_min1141(vx30, Pos(vx310), vx32, Neg(vx330), Succ(vx2540)) → new_min1166(vx30, vx310, vx32, vx330, new_not6(vx2540, new_primMulNat1(vx310, vx330)))
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min137(vx310000, vx310100, new_not3(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min197(Float(Neg(Succ(vx310000)), Pos(Succ(vx310100))), new_not9(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1141(vx30, Neg(vx310), vx32, Pos(vx330), Succ(vx2540)) → new_min145(vx30, vx310, vx32, vx330, new_not6(vx2540, new_primMulNat1(vx310, vx330)))
new_min1144(vx3010000, vx310000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min136(vx30000, vx3010000, vx310100, True) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Succ(vx30000)), Pos(Succ(vx30100)))
new_min163(vx3010000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min1155(vx310000, vx310100, new_not2(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1117(vx30000, vx3010000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min194(vx310100, new_not9(new_primPlusNat0(Zero, Succ(vx310100))))
new_min193(vx3010000, vx310000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Neg(Zero), Neg(Zero)))
new_min171(vx30000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min1170(vx19, vx200, vx21, vx220, False) → Float(Neg(Succ(vx21)), Neg(vx220))
new_min1(Float(Pos(Succ(vx30000)), vx301), Float(Pos(Succ(vx310000)), vx3101)) → new_min10(vx30000, vx301, vx310000, vx3101, new_primPlusNat1(new_primMulNat2(vx30000, vx310000), vx310000))
new_min164(vx30000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min1127(vx19, Pos(vx200), vx21, Pos(vx220), Succ(vx1410)) → new_min1106(vx19, vx200, vx21, vx220, new_not13(vx1410, vx200, vx220))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Pos(Zero), Neg(Zero))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Pos(Zero), Neg(Zero))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Neg(Zero), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Neg(Zero), Pos(Zero))
new_min1143(vx30000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min1101(vx30000, vx3010000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Pos(Succ(vx30000)), Pos(Zero))
new_min1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Pos(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Succ(vx30000)), Pos(Zero))
new_min1156(vx310000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_min136(vx30000, vx3010000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min1163(vx310100, new_not3(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1127(vx19, Pos(Zero), vx21, Neg(Succ(vx2200)), Zero) → new_min1167(vx19, vx21, vx2200, new_not9(Zero))
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min135(vx310000, vx310100, new_not9(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Neg(Succ(vx30000)), Neg(Zero))
new_min1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Neg(Zero), Neg(Succ(vx30100)))
new_min185(vx30000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min1121(vx310000, vx310100, False) → new_min01(Float(Pos(Zero), Pos(Succ(Zero))), vx310000, vx310100)
new_min165(vx19, vx2000, vx21, True) → Float(Pos(Succ(vx19)), Neg(Succ(vx2000)))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min197(Float(Neg(Zero), Pos(Succ(vx310100))), new_not9(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_primPlusNat0(Succ(vx4400), Zero) → Succ(vx4400)
new_primPlusNat0(Zero, Succ(vx3100000)) → Succ(vx3100000)
new_min1146(vx3010000, vx310000, vx310100, False) → new_min01(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), vx310000, vx310100)
new_min1127(vx19, Pos(Succ(vx2000)), vx21, Neg(Succ(vx2200)), Zero) → new_min167(vx19, vx2000, vx21, vx2200, new_not9(new_primPlusNat0(new_primMulNat1(vx2000, Succ(vx2200)), Succ(vx2200))))
new_min1132(vx30000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min1157(vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_min197(vx11, False) → vx11
new_min174(vx100, vx11, False) → vx11
new_min120(vx35, vx360, vx37, vx380, True) → Float(Neg(Succ(vx35)), Pos(vx360))
new_min1164(vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min1105(vx30000, vx3010000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min1146(vx3010000, vx310000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_min120(vx35, vx360, vx37, vx380, False) → Float(Neg(Succ(vx37)), Pos(vx380))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Neg(Zero))
new_min1103(vx3010000, vx310000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_min137(vx310000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Zero)))
new_min112(vx14, vx16, False) → new_min0(vx14, Zero, vx16, Zero)
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Neg(Zero), Neg(Zero))
new_min139(vx3010000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min157(vx30000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min192(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_min13(vx14, vx16, vx1700, True) → Float(Pos(Succ(vx14)), Pos(Zero))
new_min1127(vx19, Neg(vx200), vx21, Neg(vx220), Zero) → new_min1170(vx19, vx200, vx21, vx220, new_not11(new_primMulNat1(vx200, vx220)))
new_min1144(vx3010000, vx310000, vx310100, False) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min1130(vx30000, vx310100, new_not9(new_primPlusNat0(Zero, Succ(vx310100))))
new_min159(vx3010000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min158(vx3010000, vx310000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min10(vx14, Pos(Succ(vx1500)), vx16, Pos(Zero), Zero) → new_min12(vx14, vx1500, vx16, new_not2(Zero))
new_min138(vx310000, vx310100, False) → new_min01(Float(Pos(Zero), Neg(Succ(Zero))), vx310000, vx310100)
new_min1169(vx19, vx21, False) → Float(Neg(Succ(vx21)), Pos(Zero))
new_min146(vx3010000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min115(vx14, vx16, vx1700, False) → new_min00(vx14, Zero, vx16, Succ(vx1700))
new_min10(vx14, Pos(Succ(vx1500)), vx16, Pos(Succ(vx1700)), Succ(vx450)) → new_min11(vx14, vx1500, vx16, vx1700, new_not0(Succ(vx450), new_primPlusNat0(new_primMulNat1(vx1500, Succ(vx1700)), Succ(vx1700))))
new_min1165(vx19, vx21, False) → Float(Neg(Succ(vx21)), Neg(Zero))
new_not11(Zero) → new_not10
new_min15(vx14, vx1500, vx16, vx1700, False) → Float(Pos(Succ(vx16)), Neg(Succ(vx1700)))
new_min1135(vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_min1166(vx30, vx310, vx32, vx330, False) → Float(Pos(Succ(vx32)), Neg(vx330))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min1131(vx30000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1144(vx3010000, vx310000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min161(vx310000, vx310100, new_not3(new_primPlusNat0(Zero, Succ(vx310100))))
new_not10new_not14
new_min172(vx310000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_min134(vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_min10(vx14, Neg(Zero), vx16, Neg(Zero), Succ(vx450)) → new_min18(vx14, vx16, new_not1(vx450))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Pos(Zero), Pos(Zero))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Pos(Zero), Pos(Zero))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min136(vx30000, vx3010000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min176(vx30, vx310, vx32, vx330, False) → Float(Pos(Succ(vx32)), Pos(vx330))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Neg(Succ(vx30000)), Neg(Succ(vx30100))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min184(vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1122(vx3010000, vx310000, vx310100, False) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min154(vx3010000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1135(vx310000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Pos(Zero), Neg(Zero))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Neg(Zero), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_min180(vx3010000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_min151(vx3010000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1158(vx310000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Zero)))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Pos(Zero), Neg(Zero))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Neg(Zero), Pos(Zero))
new_min1157(vx310000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_min170(vx310000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_not5(vx3780, vx415) → new_not8
new_min1128(vx30000, vx3010000, vx310100, True) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1130(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Pos(Succ(Zero)))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min1107(vx30000, vx310100, new_not9(new_primPlusNat0(Zero, Succ(vx310100))))
new_min19(vx14, vx1500, vx16, vx1700, True) → Float(Pos(Succ(vx14)), Pos(Succ(vx1500)))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min1140(vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min169(vx30000, vx3010000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min150(vx30000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min10(vx14, Neg(Succ(vx1500)), vx16, Pos(Zero), Zero) → new_min114(vx14, vx1500, vx16, new_not3(Zero))
new_min181(vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min1129(vx30000, vx3010000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min1139(vx3010000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min118(vx30000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min175(vx310100, True) → Float(Neg(Zero), Neg(Succ(Zero)))
new_min18(vx14, vx16, False) → Float(Pos(Succ(vx16)), Neg(Zero))
new_min1(Float(Neg(Succ(vx30000)), vx301), Float(Pos(Succ(vx310000)), vx3101)) → new_min1141(vx30000, vx301, vx310000, vx3101, new_primPlusNat0(new_primMulNat1(vx30000, Succ(vx310000)), Succ(vx310000)))
new_min152(vx30000, vx3010000, vx310100, True) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_min149(vx310000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Zero)))
new_min1136(vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_min1142(vx30000, vx3010000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min1147(vx310000, vx310100, False) → new_min01(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), vx310000, vx310100)
new_not4(vx3780, Zero) → new_not8
new_not14True
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1123(vx310000, vx310100, new_not2(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min1120(vx30000, vx310100, new_not2(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min180(vx3010000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1160(vx310000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min185(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min1153(vx30000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_primMulNat2(Zero, vx310000) → Zero
new_min1141(vx30, Pos(vx310), vx32, Pos(vx330), Zero) → new_min176(vx30, vx310, vx32, vx330, new_not11(new_primMulNat1(vx310, vx330)))
new_min1108(vx310000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_min177(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min157(vx30000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min114(vx14, vx1500, vx16, False) → new_min00(vx14, Succ(vx1500), vx16, Zero)
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Pos(Zero), Neg(Zero))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Pos(Zero), Neg(Zero))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Neg(Zero), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min191(vx310100, new_not11(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min172(vx310000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min118(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_min115(vx14, vx16, vx1700, True) → Float(Pos(Succ(vx14)), Neg(Zero))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min146(vx3010000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1125(vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_min1127(vx19, Pos(vx200), vx21, Pos(vx220), Zero) → new_min1106(vx19, vx200, vx21, vx220, new_not11(new_primMulNat1(vx200, vx220)))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min1125(vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1131(vx30000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min157(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Pos(Zero), Neg(Zero))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Pos(Zero), Neg(Zero))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_min149(vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Pos(Zero), Neg(Zero))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Neg(Zero), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Neg(Zero), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Neg(Zero), Pos(Zero))
new_primMulNat1(Succ(vx2000), Succ(vx2200)) → new_primPlusNat0(new_primMulNat1(vx2000, Succ(vx2200)), Succ(vx2200))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min139(vx3010000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1118(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Neg(Succ(Zero)))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min1157(vx310000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min146(vx3010000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_primPlusNat0(Zero, Zero) → Zero
new_min151(vx3010000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min125(vx19, vx2000, vx21, False) → Float(Neg(Succ(vx21)), Neg(Zero))
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min156(vx30000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1142(vx30000, vx3010000, vx310100, True) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min179(vx310100, new_not11(new_primPlusNat0(Zero, Succ(vx310100))))
new_min10(vx14, Neg(Zero), vx16, Pos(Succ(vx1700)), Zero) → new_min115(vx14, vx16, vx1700, new_not3(Zero))
new_min1155(vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_not7(Succ(vx1860), vx1410) → new_not0(vx1860, vx1410)
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min174(vx3010000, Float(Neg(Succ(vx310000)), Pos(Succ(vx310100))), new_not9(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min168(vx5, False) → Float(Neg(Zero), Neg(Zero))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min197(Float(Pos(Succ(vx310000)), Pos(Succ(vx310100))), new_not3(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1113(vx30000, vx3010000, vx310100, True) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1138(vx310000, vx310100, new_not11(new_primPlusNat0(Zero, Succ(vx310100))))
new_not0(Succ(vx37800), Zero) → new_not8
new_min1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Pos(Zero), Neg(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Pos(Succ(vx30000)), Neg(Zero))
new_min1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Pos(Zero), Neg(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Pos(Succ(vx30000)), Neg(Zero))
new_min1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Neg(Succ(vx30000)), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Neg(Zero), Pos(Succ(vx30100)))
new_min1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Neg(Succ(vx30000)), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Neg(Zero), Pos(Succ(vx30100)))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min1110(vx3010000, vx310000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min155(vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min1153(vx30000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min1133(vx3010000, vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_min110(vx14, vx1500, vx16, True) → Float(Pos(Succ(vx14)), Pos(Succ(vx1500)))
new_min130(vx30000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_primPlusNat1(Succ(vx440), vx310000) → Succ(Succ(new_primPlusNat0(vx440, vx310000)))
new_min160(vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min1126(vx310100, True) → Float(Pos(Zero), Neg(Succ(Zero)))
new_min148(vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_min169(vx30000, vx3010000, vx310100, True) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min129(vx310100, new_not3(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1149(vx3010000, vx310000, vx310100, False) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_min1160(vx310000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_min1130(vx30000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_not1(vx450) → new_not8
new_min128(vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_min119(vx35, Neg(vx360), vx37, Pos(vx380), Zero) → new_min122(vx35, vx360, vx37, vx380, new_not3(new_primMulNat1(vx360, vx380)))
new_min156(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_min152(vx30000, vx3010000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min10(vx14, Pos(Zero), vx16, Pos(Zero), Succ(vx450)) → new_min14(vx14, vx16, new_not1(vx450))
new_min1110(vx3010000, vx310000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min1129(vx30000, vx3010000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min183(vx8) → vx8
new_min10(vx14, Pos(Zero), vx16, Pos(Succ(vx1700)), Succ(vx450)) → new_min13(vx14, vx16, vx1700, new_not1(vx450))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min134(vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min199(vx30000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min174(vx3010000, Float(Pos(Succ(vx310000)), Pos(Succ(vx310100))), new_not3(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min11(vx14, vx1500, vx16, vx1700, False) → new_min01(Float(Pos(Succ(vx14)), Pos(Succ(vx1500))), vx16, vx1700)
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min1161(vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min179(vx310100, True) → Float(Pos(Zero), Pos(Succ(Zero)))
new_min1141(vx30, Pos(vx310), vx32, Neg(vx330), Zero) → new_min1166(vx30, vx310, vx32, vx330, new_not9(new_primMulNat1(vx310, vx330)))
new_min1113(vx30000, vx3010000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min1120(vx30000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min11(vx14, vx1500, vx16, vx1700, True) → Float(Pos(Succ(vx14)), Pos(Succ(vx1500)))
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1100(vx310000, vx310100, new_not9(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min174(vx3010000, Float(Pos(Zero), Pos(Succ(vx310100))), new_not3(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min196(vx19, vx2000, vx21, vx2200, False) → Float(Neg(Succ(vx21)), Pos(Succ(vx2200)))
new_min1106(vx19, vx200, vx21, vx220, True) → Float(Pos(Succ(vx19)), Pos(vx200))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min164(vx30000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min1116(vx30000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_not0(Zero, Succ(vx40700)) → new_not12
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min117(vx30000, vx310100, new_not11(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min173(vx310000, vx310100, new_not11(new_primPlusNat0(Zero, Succ(vx310100))))
new_min142(vx30000, vx3010000, vx310100, True) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_min135(vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min174(vx3010000, Float(Neg(Zero), Pos(Succ(vx310100))), new_not9(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min10(vx14, Neg(Succ(vx1500)), vx16, Pos(Succ(vx1700)), Zero) → new_min113(vx14, vx1500, vx16, vx1700, new_not3(new_primPlusNat0(new_primMulNat1(vx1500, Succ(vx1700)), Succ(vx1700))))
new_min1148(vx310000, vx310100, False) → new_min01(Float(Neg(Zero), Neg(Succ(Zero))), vx310000, vx310100)
new_min142(vx30000, vx3010000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min187(vx310000, vx310100, False) → new_min01(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), vx310000, vx310100)
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1134(vx3010000, vx310000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min1147(vx310000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min123(vx35, vx360, vx37, vx380, False) → Float(Neg(Succ(vx37)), Neg(vx380))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min1118(vx30000, vx310100, new_not3(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1132(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_min1127(vx19, Neg(Zero), vx21, Pos(Zero), Zero) → new_min1169(vx19, vx21, new_not9(Zero))
new_min0(vx14, vx150, vx16, vx170) → Float(Pos(Succ(vx16)), Neg(vx170))
new_min128(vx310000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_min1122(vx3010000, vx310000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min175(vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Neg(Zero), Pos(Zero)))
new_min1138(vx310000, vx310100, True) → Float(Pos(Zero), Neg(Succ(Zero)))
new_min1163(vx310100, True) → Float(Neg(Zero), Neg(Succ(Zero)))
new_min1127(vx19, Neg(Zero), vx21, Pos(Succ(vx2200)), Succ(vx1410)) → new_min1168(vx19, vx21, vx2200, new_not7(Zero, vx1410))
new_min143(vx30, vx310, vx32, vx330, True) → Float(Neg(Succ(vx30)), Neg(vx310))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Pos(Zero), Pos(Zero))
new_min1119(vx30000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min119(vx35, Neg(vx360), vx37, Neg(vx380), Succ(vx3780)) → new_min123(vx35, vx360, vx37, vx380, new_not4(vx3780, new_primMulNat1(vx360, vx380)))
new_min1166(vx30, vx310, vx32, vx330, True) → Float(Neg(Succ(vx30)), Pos(vx310))
new_min1158(vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_min1168(vx19, vx21, vx2200, True) → Float(Pos(Succ(vx19)), Neg(Zero))
new_min1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Pos(Succ(vx30000)), Neg(Zero))
new_min1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Succ(vx30000)), Neg(Zero))
new_min1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Pos(Zero), Neg(Succ(vx30100)))
new_min1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Neg(Succ(vx30000)), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Neg(Zero), Pos(Succ(vx30100)))
new_min1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Succ(vx30000)), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Succ(vx30100)))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min174(vx3010000, Float(Pos(Zero), Neg(Succ(vx310100))), new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Pos(Zero), Neg(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Pos(Succ(vx30000)), Neg(Zero))
new_min1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Neg(Succ(vx30000)), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Neg(Zero), Pos(Succ(vx30100)))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min166(vx3010000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1114(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Pos(Succ(Zero)))
new_min194(vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min10(vx14, Neg(Succ(vx1500)), vx16, Neg(Zero), Zero) → new_min16(vx14, vx1500, vx16, new_not2(Zero))
new_min1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min199(vx30000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min121(vx35, vx360, vx37, vx380, True) → Float(Neg(Succ(vx35)), Pos(vx360))
new_min10(vx14, Neg(Succ(vx1500)), vx16, Neg(Succ(vx1700)), Succ(vx450)) → new_min15(vx14, vx1500, vx16, vx1700, new_not0(Succ(vx450), new_primPlusNat0(new_primMulNat1(vx1500, Succ(vx1700)), Succ(vx1700))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min170(vx310000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min161(vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min175(vx310100, new_not2(new_primPlusNat0(Zero, Succ(vx310100))))
new_min10(vx14, Neg(Succ(vx1500)), vx16, Neg(Succ(vx1700)), Zero) → new_min15(vx14, vx1500, vx16, vx1700, new_not2(new_primPlusNat0(new_primMulNat1(vx1500, Succ(vx1700)), Succ(vx1700))))
new_min1127(vx19, Neg(vx200), vx21, Neg(vx220), Succ(vx1410)) → new_min1170(vx19, vx200, vx21, vx220, new_not13(vx1410, vx200, vx220))
new_min147(vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_min1127(vx19, Pos(Zero), vx21, Neg(Succ(vx2200)), Succ(vx1410)) → new_min1167(vx19, vx21, vx2200, new_not7(Zero, vx1410))
new_min10(vx14, Pos(Succ(vx1500)), vx16, Neg(Zero), Zero) → new_min110(vx14, vx1500, vx16, new_not3(Zero))
new_min1118(vx30000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1149(vx3010000, vx310000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min1139(vx3010000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Pos(Succ(vx30000)), vx301), Float(Neg(Succ(vx310000)), vx3101)) → new_min1127(vx30000, vx301, vx310000, vx3101, new_primPlusNat0(new_primMulNat2(vx30000, vx310000), Succ(vx310000)))
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min138(vx310000, vx310100, new_not3(new_primPlusNat0(Zero, Succ(vx310100))))
new_min159(vx3010000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min1158(vx310000, vx310100, new_not3(new_primPlusNat0(Zero, Succ(vx310100))))
new_min162(vx30000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min163(vx3010000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Neg(Succ(vx30000)), Neg(Zero))
new_min1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Neg(Zero), Neg(Succ(vx30100)))
new_min1145(vx310000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_min184(vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_min1127(vx19, Pos(Succ(vx2000)), vx21, Neg(Zero), Succ(vx1410)) → new_min125(vx19, vx2000, vx21, new_not7(Zero, vx1410))
new_primMulNat1(Succ(vx2000), Zero) → Zero
new_primMulNat1(Zero, Succ(vx2200)) → Zero
new_min17(vx14, vx16, vx1700, False) → Float(Pos(Succ(vx16)), Neg(Succ(vx1700)))
new_min156(vx30000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Pos(Zero), Pos(Zero))
new_min1110(vx3010000, vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_min1140(vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min1146(vx3010000, vx310000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min1151(vx3010000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Pos(Zero), Pos(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Pos(Succ(vx30000)), Pos(Zero))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min149(vx310000, vx310100, new_not2(new_primPlusNat0(Zero, Succ(vx310100))))
new_min119(vx35, Neg(vx360), vx37, Neg(vx380), Zero) → new_min123(vx35, vx360, vx37, vx380, new_not2(new_primMulNat1(vx360, vx380)))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min197(Float(Pos(Succ(vx310000)), Neg(Succ(vx310100))), new_not2(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1114(vx30000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_not11(Succ(vx1840)) → new_not12
new_min1111(vx310100, True) → Float(Pos(Zero), Neg(Succ(Zero)))
new_min145(vx30, vx310, vx32, vx330, True) → Float(Neg(Succ(vx30)), Neg(vx310))
new_min1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Neg(Succ(vx30100)))
new_min1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Succ(vx30000)), Neg(Zero))
new_not6(vx2540, vx286) → new_not7(vx286, vx2540)
new_min1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Neg(Succ(vx30000)), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1145(vx310000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Succ(vx30100)))
new_primPlusNat0(Succ(vx4400), Succ(vx3100000)) → Succ(Succ(new_primPlusNat0(vx4400, vx3100000)))
new_min1134(vx3010000, vx310000, vx310100, False) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Pos(Zero), Pos(Zero))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_min145(vx30, vx310, vx32, vx330, False) → Float(Pos(Succ(vx32)), Pos(vx330))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1102(vx310000, vx310100, new_not11(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1124(vx3010000, vx310100, True) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1154(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Neg(Succ(Zero)))
new_min1127(vx19, Pos(Zero), vx21, Neg(Zero), Zero) → new_min1165(vx19, vx21, new_not9(Zero))
new_min10(vx14, Neg(Zero), vx16, Neg(Succ(vx1700)), Succ(vx450)) → new_min17(vx14, vx16, vx1700, new_not1(vx450))
new_min119(vx35, Pos(vx360), vx37, Neg(vx380), Succ(vx3780)) → new_min121(vx35, vx360, vx37, vx380, new_not5(vx3780, new_primMulNat1(vx360, vx380)))
new_min163(vx3010000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min133(vx30000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min1165(vx19, vx21, True) → Float(Pos(Succ(vx19)), Pos(Zero))
new_min188(vx30000, vx3010000, vx310100, True) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_min141(vx310000, vx310100, new_not11(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min1111(vx310100, new_not9(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Succ(vx30000)), Neg(Succ(vx30100)))
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Neg(Succ(vx30000)), Pos(Succ(vx30100)))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min148(vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min182(vx3010000, vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min131(vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_not13(vx1410, vx200, vx220) → new_not12
new_min147(vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min178(vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Pos(Zero), Neg(Zero))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Neg(Zero), Pos(Zero))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Neg(Zero), Pos(Zero))
new_min1127(vx19, Pos(Succ(vx2000)), vx21, Neg(Succ(vx2200)), Succ(vx1410)) → new_min167(vx19, vx2000, vx21, vx2200, new_not7(new_primPlusNat0(new_primMulNat1(vx2000, Succ(vx2200)), Succ(vx2200)), vx1410))
new_min192(vx30000, vx310100, False) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_min131(vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_min167(vx19, vx2000, vx21, vx2200, False) → Float(Neg(Succ(vx21)), Neg(Succ(vx2200)))
new_not8False
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Neg(Zero), Neg(Zero))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Neg(Zero), Neg(Zero))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(vx301000)))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_min1137(vx301000, Float(Neg(Succ(vx310000)), Neg(Succ(vx310100))), vx310100)
new_min154(vx3010000, vx310100, True) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_min166(vx3010000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Pos(Succ(vx30000)), Neg(Succ(vx30100))))
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Neg(Succ(vx30000)), Pos(Succ(vx30100))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_min131(vx310100, new_not3(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Pos(Zero))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min1124(vx3010000, vx310100, new_not2(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_not0(Succ(vx37800), Succ(vx40700)) → new_not0(vx37800, vx40700)
new_not3(Succ(vx4160)) → new_not8
new_min119(vx35, Pos(vx360), vx37, Neg(vx380), Zero) → new_min121(vx35, vx360, vx37, vx380, new_not3(new_primMulNat1(vx360, vx380)))
new_min1101(vx30000, vx3010000, vx310100, True) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_min122(vx35, vx360, vx37, vx380, False) → Float(Neg(Succ(vx37)), Pos(vx380))
new_min1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_min162(vx30000, vx310100, new_not11(new_primPlusNat0(new_primPlusNat0(Zero, Succ(vx310100)), Succ(vx310100))))
new_min18(vx14, vx16, True) → Float(Pos(Succ(vx14)), Neg(Zero))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min153(vx310100, new_not11(new_primPlusNat0(Zero, Succ(vx310100))))
new_min117(vx30000, vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min137(vx310000, vx310100, False) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min127(vx310100, new_not9(new_primPlusNat0(Zero, Succ(vx310100))))
new_min1126(vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min1(Float(Pos(Succ(vx30000)), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_min190(vx30000, vx310100, new_not3(new_primPlusNat0(Zero, Succ(vx310100))))
new_min179(vx310100, False) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_min1131(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_min1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_min142(vx30000, vx3010000, vx310100, new_not9(new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_min111(vx14, vx16, vx1700, False) → new_min0(vx14, Zero, vx16, Succ(vx1700))
new_min187(vx310000, vx310100, True) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_min195(vx30000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min126(vx30000, vx3010000, vx310100, True) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_min1120(vx30000, vx310100, True) → Float(Pos(Succ(vx30000)), Neg(Succ(Zero)))
new_min150(vx30000, vx310100, True) → Float(Neg(Succ(vx30000)), Neg(Succ(Zero)))
new_min1117(vx30000, vx3010000, vx310100, True) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_min1151(vx3010000, vx310100, False) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_min1124(vx3010000, vx310100, False) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_min1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Pos(Zero), Neg(Succ(vx30100))))
new_min1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Neg(Succ(vx30000)), Pos(Zero)))
new_min1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_min183(Float(Neg(Zero), Pos(Succ(vx30100))))

The set Q consists of the following terms:

new_min176(x0, x1, x2, x3, True)
new_min10(x0, Neg(Zero), x1, Neg(Succ(x2)), Zero)
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Succ(x0))))
new_not0(Succ(x0), Zero)
new_min10(x0, Pos(Succ(x1)), x2, Pos(Zero), Succ(x3))
new_min116(x0, x1, False)
new_min1105(x0, x1, x2, True)
new_min1(Float(Pos(Zero), Neg(Succ(x0))), Float(Pos(Zero), Pos(Zero)))
new_min1(Float(Neg(Zero), Pos(Succ(x0))), Float(Pos(Zero), Pos(Zero)))
new_min118(x0, x1, False)
new_min1(Float(Pos(Zero), Pos(Succ(x0))), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Pos(Zero), Pos(Succ(x0))), Float(Neg(Zero), Pos(Zero)))
new_min163(x0, x1, False)
new_min114(x0, x1, x2, False)
new_min1(Float(Neg(Succ(x0)), Neg(Succ(x1))), Float(Neg(Zero), Neg(Zero)))
new_min122(x0, x1, x2, x3, True)
new_min136(x0, x1, x2, False)
new_min181(x0, False)
new_min1(Float(Pos(Zero), Neg(Succ(x0))), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Pos(Zero), Neg(Succ(x0))), Float(Neg(Zero), Pos(Zero)))
new_min1(Float(Neg(Zero), Pos(Succ(x0))), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Neg(Zero), Pos(Succ(x0))), Float(Neg(Zero), Pos(Zero)))
new_min1(Float(Pos(Zero), Pos(Succ(x0))), Float(Neg(Zero), Neg(Zero)))
new_min1(Float(Neg(Zero), Neg(Succ(x0))), Float(Pos(Zero), Pos(Zero)))
new_not8
new_min1101(x0, x1, x2, True)
new_min129(x0, True)
new_min1107(x0, x1, False)
new_min154(x0, x1, True)
new_min127(x0, False)
new_min177(x0, x1, False)
new_min1161(x0, False)
new_min1163(x0, True)
new_min1157(x0, x1, False)
new_min1119(x0, x1, True)
new_min1134(x0, x1, x2, True)
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Neg(Succ(x0)), x1), Float(Neg(Succ(x2)), x3))
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Neg(Succ(x0))), Float(Neg(Zero), Neg(Zero)))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Pos(Succ(x2))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Neg(Succ(x2))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Succ(x1)), Pos(Succ(x2))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Pos(Succ(x2))))
new_min1120(x0, x1, True)
new_min0(x0, x1, x2, x3)
new_min12(x0, x1, x2, False)
new_min125(x0, x1, x2, False)
new_min15(x0, x1, x2, x3, True)
new_min1117(x0, x1, x2, True)
new_min1129(x0, x1, x2, True)
new_min134(x0, False)
new_min1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Neg(Zero)))
new_min119(x0, Neg(x1), x2, Neg(x3), Succ(x4))
new_min174(x0, x1, True)
new_min1147(x0, x1, False)
new_min1139(x0, x1, False)
new_min130(x0, x1, False)
new_min1145(x0, x1, False)
new_min1154(x0, x1, False)
new_min189(x0, x1, False)
new_primPlusNat0(Zero, Succ(x0))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Succ(x0))))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Succ(x0))))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Succ(x0))))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Succ(x0))))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Succ(x0))))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Succ(x0))))
new_min1103(x0, x1, x2, True)
new_min1168(x0, x1, x2, True)
new_min146(x0, x1, False)
new_min18(x0, x1, False)
new_min1165(x0, x1, False)
new_min136(x0, x1, x2, True)
new_min180(x0, x1, False)
new_min1106(x0, x1, x2, x3, True)
new_min180(x0, x1, True)
new_min164(x0, x1, False)
new_min10(x0, Pos(Succ(x1)), x2, Pos(Zero), Zero)
new_min1152(x0, True)
new_min1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(x1))))
new_min1161(x0, True)
new_min1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Pos(Zero)))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x0))))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x0))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x0))))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x0))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x0))))
new_min159(x0, x1, True)
new_min1127(x0, Pos(Succ(x1)), x2, Neg(Zero), Zero)
new_min1127(x0, Neg(Succ(x1)), x2, Pos(Zero), Zero)
new_min1(Float(Pos(Zero), Neg(Succ(x0))), Float(Neg(Zero), Neg(Zero)))
new_min1(Float(Neg(Zero), Pos(Succ(x0))), Float(Neg(Zero), Neg(Zero)))
new_min1(Float(Neg(Zero), Neg(Succ(x0))), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Neg(Zero), Neg(Succ(x0))), Float(Neg(Zero), Pos(Zero)))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(x0)))), Float(Neg(Zero), Neg(Succ(x1))))
new_min1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Pos(Succ(x2))))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_min135(x0, x1, False)
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_min147(x0, False)
new_min124(x0, x1, False)
new_min131(x0, True)
new_min140(x0, x1, x2, False)
new_min129(x0, False)
new_min1(Float(Pos(Zero), Pos(Succ(x0))), Float(Pos(Zero), Pos(Zero)))
new_min1143(x0, x1, False)
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Zero)))
new_min1157(x0, x1, True)
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Zero)))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Zero)))
new_min120(x0, x1, x2, x3, True)
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x0))))
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x0))))
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x0))))
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x0))))
new_min1127(x0, Neg(Succ(x1)), x2, Pos(Succ(x3)), Zero)
new_min188(x0, x1, x2, False)
new_min1127(x0, Pos(Succ(x1)), x2, Neg(Succ(x3)), Zero)
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Succ(x0))))
new_min116(x0, x1, True)
new_min1(Float(Pos(Zero), Pos(Succ(x0))), Float(Neg(Succ(x1)), Neg(Zero)))
new_min1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Neg(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Succ(x0))), Float(Neg(Succ(x1)), Pos(Zero)))
new_min1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Succ(x0))), Float(Pos(Succ(x1)), Neg(Zero)))
new_min1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Pos(Succ(x0))), Float(Pos(Succ(x1)), Neg(Zero)))
new_min1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Pos(Succ(x1))))
new_min1(Float(Neg(Zero), Pos(Succ(x0))), Float(Neg(Succ(x1)), Pos(Zero)))
new_min1(Float(Neg(Zero), Neg(Succ(x0))), Float(Pos(Succ(x1)), Pos(Zero)))
new_min1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Pos(Succ(x1))))
new_min149(x0, x1, False)
new_not3(Succ(x0))
new_min10(x0, Pos(Zero), x1, Pos(Zero), Zero)
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x0))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x0))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(x0))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x0))))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x0))))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x0))))
new_min1168(x0, x1, x2, False)
new_min157(x0, x1, False)
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Neg(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Zero), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Pos(Succ(x1))))
new_min132(x0, False)
new_min187(x0, x1, False)
new_min1149(x0, x1, x2, False)
new_min168(x0, True)
new_min185(x0, x1, True)
new_min111(x0, x1, x2, True)
new_min1141(x0, Neg(x1), x2, Neg(x3), Zero)
new_min119(x0, Pos(x1), x2, Neg(x3), Succ(x4))
new_min119(x0, Neg(x1), x2, Pos(x3), Succ(x4))
new_min185(x0, x1, False)
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Neg(Zero)))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Neg(Zero)))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Neg(Zero), Pos(Succ(x1))))
new_primMulNat1(Zero, Zero)
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Neg(Zero)))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Pos(Zero)))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Zero), Neg(Succ(x1))))
new_min1131(x0, x1, True)
new_min166(x0, x1, True)
new_min1150(x0, x1, True)
new_min117(x0, x1, False)
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Neg(Zero)))
new_min1167(x0, x1, x2, True)
new_min1158(x0, x1, True)
new_min178(x0, True)
new_min1137(Succ(x0), x1, x2)
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Pos(Zero)))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Neg(Zero)))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Neg(Zero)))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Pos(Zero)))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Neg(Zero)))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Pos(Zero)))
new_min171(x0, x1, False)
new_min1(Float(Pos(Succ(x0)), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Pos(Succ(x0)), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Succ(x0)), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x1))))
new_min1(Float(Neg(Succ(x0)), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x1))))
new_min1127(x0, Pos(x1), x2, Pos(x3), Succ(x4))
new_min17(x0, x1, x2, True)
new_min17(x0, x1, x2, False)
new_min1110(x0, x1, x2, False)
new_min1141(x0, Pos(x1), x2, Neg(x3), Zero)
new_min1141(x0, Neg(x1), x2, Pos(x3), Zero)
new_min1133(x0, x1, x2, False)
new_min115(x0, x1, x2, True)
new_min1146(x0, x1, x2, True)
new_min1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x1))))
new_min1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(x1))))
new_min113(x0, x1, x2, x3, False)
new_min1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(x1))))
new_min138(x0, x1, True)
new_min1140(x0, False)
new_min10(x0, Pos(Succ(x1)), x2, Pos(Succ(x3)), Zero)
new_min155(x0, False)
new_min153(x0, True)
new_min1112(x0, x1, x2, True)
new_min1(Float(Pos(Succ(x0)), Neg(Succ(x1))), Float(Neg(Zero), Pos(Zero)))
new_min1(Float(Pos(Succ(x0)), Neg(Succ(x1))), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Neg(Succ(x0)), Pos(Succ(x1))), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Neg(Succ(x0)), Pos(Succ(x1))), Float(Neg(Zero), Pos(Zero)))
new_min1(Float(Neg(Succ(x0)), Neg(Succ(x1))), Float(Pos(Zero), Pos(Zero)))
new_min1(Float(Pos(Succ(x0)), Pos(Succ(x1))), Float(Neg(Zero), Neg(Zero)))
new_min1135(x0, x1, False)
new_min1127(x0, Neg(Zero), x1, Pos(Succ(x2)), Zero)
new_min1127(x0, Pos(Zero), x1, Neg(Succ(x2)), Zero)
new_min186(x0, False)
new_min1(Float(Pos(Succ(x0)), Neg(Succ(x1))), Float(Neg(Zero), Neg(Zero)))
new_min1(Float(Neg(Succ(x0)), Pos(Succ(x1))), Float(Neg(Zero), Neg(Zero)))
new_min1(Float(Neg(Succ(x0)), Neg(Succ(x1))), Float(Neg(Zero), Pos(Zero)))
new_min1(Float(Neg(Succ(x0)), Neg(Succ(x1))), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Neg(Zero)))
new_min1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Pos(Zero)))
new_min1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Neg(Zero)))
new_min128(x0, x1, True)
new_min173(x0, x1, True)
new_min1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Pos(Succ(x0))), Float(Pos(Succ(x1)), Pos(Zero)))
new_min1169(x0, x1, False)
new_min1151(x0, x1, False)
new_primMulNat2(Zero, x0)
new_min133(x0, x1, False)
new_min110(x0, x1, x2, False)
new_min126(x0, x1, x2, False)
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_min1147(x0, x1, True)
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_min1116(x0, x1, True)
new_min16(x0, x1, x2, False)
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_min1141(x0, Neg(x1), x2, Neg(x3), Succ(x4))
new_not2(Succ(x0))
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_min115(x0, x1, x2, False)
new_min1162(x0, False)
new_min199(x0, x1, True)
new_min1116(x0, x1, False)
new_min181(x0, True)
new_min1104(x0, x1, False)
new_min1164(x0, False)
new_min1160(x0, x1, True)
new_min192(x0, x1, False)
new_min1102(x0, x1, False)
new_min1128(x0, x1, x2, True)
new_min1118(x0, x1, False)
new_min165(x0, x1, x2, True)
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Pos(Zero)))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Pos(Zero)))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Pos(Zero)))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Neg(Zero)))
new_primMulNat1(Succ(x0), Zero)
new_min175(x0, False)
new_min1113(x0, x1, x2, False)
new_min1126(x0, True)
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_min160(x0, False)
new_min1115(x0, x1, x2, False)
new_min1148(x0, x1, True)
new_min137(x0, x1, False)
new_min131(x0, False)
new_min1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Pos(Succ(x2))))
new_min1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Neg(Succ(x2))))
new_min1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Neg(Succ(x2))))
new_min1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Neg(Succ(x2))))
new_min1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Pos(Succ(x2))))
new_min1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Pos(Succ(x2))))
new_min151(x0, x1, True)
new_min1102(x0, x1, True)
new_min148(x0, True)
new_min176(x0, x1, x2, x3, False)
new_min127(x0, True)
new_min164(x0, x1, True)
new_min1133(x0, x1, x2, True)
new_min1160(x0, x1, False)
new_min10(x0, Neg(x1), x2, Pos(x3), Succ(x4))
new_min10(x0, Pos(x1), x2, Neg(x3), Succ(x4))
new_min1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Neg(Succ(x2))))
new_min1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Pos(Succ(x2))))
new_min1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Neg(Succ(x2))))
new_min1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Neg(Succ(x2))))
new_min124(x0, x1, True)
new_min1141(x0, Pos(x1), x2, Neg(x3), Succ(x4))
new_min1141(x0, Neg(x1), x2, Pos(x3), Succ(x4))
new_min1122(x0, x1, x2, True)
new_min187(x0, x1, True)
new_min194(x0, False)
new_min1156(x0, x1, True)
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1142(x0, x1, x2, False)
new_min1(Float(Pos(Succ(x0)), x1), Float(Pos(Succ(x2)), x3))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Succ(x0))))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Succ(x0))))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Succ(x0))))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Succ(x0))))
new_min118(x0, x1, True)
new_min166(x0, x1, False)
new_primMulNat1(Zero, Succ(x0))
new_min144(x0, False)
new_min10(x0, Neg(Succ(x1)), x2, Neg(Succ(x3)), Succ(x4))
new_min123(x0, x1, x2, x3, True)
new_min14(x0, x1, True)
new_min1105(x0, x1, x2, False)
new_min13(x0, x1, x2, True)
new_min1127(x0, Pos(Zero), x1, Neg(Succ(x2)), Succ(x3))
new_min1127(x0, Neg(Zero), x1, Pos(Succ(x2)), Succ(x3))
new_min1120(x0, x1, False)
new_min110(x0, x1, x2, True)
new_min1(Float(Pos(Zero), Neg(Succ(x0))), Float(Neg(Succ(x1)), Neg(Zero)))
new_min1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Neg(Succ(x1))))
new_min1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Pos(Succ(x0))), Float(Neg(Succ(x1)), Neg(Zero)))
new_min1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Neg(Succ(x0))), Float(Pos(Succ(x1)), Neg(Zero)))
new_min1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Pos(Succ(x1))))
new_min1(Float(Neg(Zero), Neg(Succ(x0))), Float(Neg(Succ(x1)), Pos(Zero)))
new_min1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Neg(Succ(x2))))
new_min1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Pos(Succ(x2))))
new_min1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Pos(Succ(x2))))
new_min1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Pos(Succ(x2))))
new_min10(x0, Pos(Zero), x1, Pos(Succ(x2)), Succ(x3))
new_min1167(x0, x1, x2, False)
new_min1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Pos(Zero)))
new_min1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Pos(Zero)))
new_min179(x0, True)
new_min1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Neg(Zero)))
new_min1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Pos(Zero)))
new_min1121(x0, x1, True)
new_primPlusNat0(Zero, Zero)
new_min172(x0, x1, True)
new_min130(x0, x1, True)
new_min1113(x0, x1, x2, True)
new_min1141(x0, Pos(x1), x2, Pos(x3), Succ(x4))
new_min119(x0, Pos(x1), x2, Neg(x3), Zero)
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_min119(x0, Neg(x1), x2, Pos(x3), Zero)
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_min121(x0, x1, x2, x3, True)
new_min143(x0, x1, x2, x3, False)
new_min1127(x0, Neg(x1), x2, Neg(x3), Succ(x4))
new_primMulNat2(Succ(x0), x1)
new_min1125(x0, False)
new_min1155(x0, x1, True)
new_min175(x0, True)
new_min120(x0, x1, x2, x3, False)
new_min1137(Zero, x0, x1)
new_min1152(x0, False)
new_min1119(x0, x1, False)
new_min1162(x0, True)
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_min160(x0, True)
new_min170(x0, x1, False)
new_min162(x0, x1, False)
new_min1169(x0, x1, True)
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Succ(x0))))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Succ(x0))))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Succ(x0))))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Succ(x0))))
new_min126(x0, x1, x2, True)
new_min155(x0, True)
new_min119(x0, Pos(x1), x2, Pos(x3), Succ(x4))
new_min1150(x0, x1, False)
new_min1117(x0, x1, x2, False)
new_min1126(x0, False)
new_min198(x0, x1, x2, False)
new_min10(x0, Neg(Zero), x1, Neg(Succ(x2)), Succ(x3))
new_min10(x0, Pos(Succ(x1)), x2, Neg(Zero), Zero)
new_min10(x0, Neg(Succ(x1)), x2, Neg(Succ(x3)), Zero)
new_min10(x0, Neg(Succ(x1)), x2, Pos(Zero), Zero)
new_min1156(x0, x1, False)
new_min1111(x0, False)
new_min1(Float(Pos(Zero), Neg(Succ(Succ(x0)))), Float(Neg(Succ(x1)), Neg(Succ(x2))))
new_not4(x0, Zero)
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Zero)))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Neg(Succ(x2))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Neg(Succ(x1)), Pos(Succ(x2))))
new_min1149(x0, x1, x2, True)
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Succ(x1)), Neg(Succ(x2))))
new_min1(Float(Neg(Succ(x0)), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Succ(x0)), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x1))))
new_min1(Float(Neg(Succ(x0)), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x1))))
new_min1(Float(Neg(Succ(x0)), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x1))))
new_min10(x0, Pos(Succ(x1)), x2, Pos(Succ(x3)), Succ(x4))
new_min19(x0, x1, x2, x3, True)
new_min121(x0, x1, x2, x3, False)
new_min1135(x0, x1, True)
new_min156(x0, x1, True)
new_min150(x0, x1, True)
new_min10(x0, Pos(Zero), x1, Pos(Zero), Succ(x2))
new_min1114(x0, x1, False)
new_min197(x0, True)
new_min1143(x0, x1, True)
new_min178(x0, False)
new_min177(x0, x1, True)
new_min1109(x0, x1, False)
new_min199(x0, x1, False)
new_min165(x0, x1, x2, False)
new_min1170(x0, x1, x2, x3, False)
new_min119(x0, Pos(x1), x2, Pos(x3), Zero)
new_not12
new_min1153(x0, x1, True)
new_min193(x0, x1, x2, False)
new_min1144(x0, x1, x2, True)
new_min188(x0, x1, x2, True)
new_min134(x0, True)
new_min148(x0, False)
new_min159(x0, x1, False)
new_primPlusNat0(Succ(x0), Succ(x1))
new_min1131(x0, x1, False)
new_min18(x0, x1, True)
new_min184(x0, False)
new_min1145(x0, x1, True)
new_min10(x0, Neg(Zero), x1, Pos(Zero), Zero)
new_min10(x0, Pos(Zero), x1, Neg(Zero), Zero)
new_min1112(x0, x1, x2, False)
new_min154(x0, x1, False)
new_primPlusNat1(Zero, x0)
new_min1123(x0, x1, False)
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x0))))
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x0))))
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x0))))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x0))))
new_min1153(x0, x1, False)
new_min152(x0, x1, x2, True)
new_not14
new_primMulNat1(Succ(x0), Succ(x1))
new_min1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Pos(Zero)))
new_min1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Pos(Zero)))
new_min1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Pos(Zero)))
new_min1166(x0, x1, x2, x3, False)
new_min01(x0, x1, x2)
new_not7(Zero, x0)
new_min197(x0, False)
new_min167(x0, x1, x2, x3, False)
new_min11(x0, x1, x2, x3, False)
new_min169(x0, x1, x2, True)
new_min157(x0, x1, True)
new_min111(x0, x1, x2, False)
new_min1134(x0, x1, x2, False)
new_min1159(x0, x1, x2, False)
new_min1100(x0, x1, True)
new_min1(Float(Pos(Succ(x0)), Neg(Succ(x1))), Float(Pos(Zero), Pos(Zero)))
new_min1(Float(Neg(Succ(x0)), Pos(Succ(x1))), Float(Pos(Zero), Pos(Zero)))
new_min1(Float(Pos(Succ(x0)), Pos(Succ(x1))), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Pos(Succ(x0)), Pos(Succ(x1))), Float(Neg(Zero), Pos(Zero)))
new_min1121(x0, x1, False)
new_min1159(x0, x1, x2, True)
new_min1(Float(Neg(Succ(x0)), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x1))))
new_not2(Zero)
new_min1(Float(Pos(Succ(x0)), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_min158(x0, x1, x2, True)
new_min1124(x0, x1, True)
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Pos(Succ(x2))))
new_min1142(x0, x1, x2, True)
new_min167(x0, x1, x2, x3, True)
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Zero)))
new_min1111(x0, True)
new_min1127(x0, Pos(Succ(x1)), x2, Neg(Succ(x3)), Succ(x4))
new_min141(x0, x1, False)
new_min1127(x0, Neg(Succ(x1)), x2, Pos(Succ(x3)), Succ(x4))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_not0(Zero, Succ(x0))
new_min1136(x0, x1, False)
new_min1144(x0, x1, x2, False)
new_not13(x0, x1, x2)
new_min171(x0, x1, True)
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x0))))
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x0))))
new_min1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x0))))
new_min1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x0))))
new_min1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x0))))
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x0))))
new_not11(Succ(x0))
new_min122(x0, x1, x2, x3, False)
new_min15(x0, x1, x2, x3, False)
new_min1114(x0, x1, True)
new_min1154(x0, x1, True)
new_min10(x0, Neg(Zero), x1, Pos(Succ(x2)), Zero)
new_min10(x0, Pos(Zero), x1, Neg(Succ(x2)), Zero)
new_min1109(x0, x1, True)
new_not7(Succ(x0), x1)
new_min146(x0, x1, True)
new_min139(x0, x1, True)
new_min1166(x0, x1, x2, x3, True)
new_min142(x0, x1, x2, True)
new_min10(x0, Neg(Zero), x1, Neg(Zero), Succ(x2))
new_min190(x0, x1, False)
new_not9(Succ(x0))
new_min1141(x0, Pos(x1), x2, Pos(x3), Zero)
new_min151(x0, x1, False)
new_min1123(x0, x1, True)
new_min123(x0, x1, x2, x3, False)
new_min1132(x0, x1, True)
new_min13(x0, x1, x2, False)
new_min117(x0, x1, True)
new_not4(x0, Succ(x1))
new_min1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Neg(Succ(x2))))
new_min144(x0, True)
new_min00(x0, x1, x2, x3)
new_min172(x0, x1, False)
new_min1127(x0, Pos(Zero), x1, Neg(Zero), Succ(x2))
new_min1127(x0, Neg(Zero), x1, Pos(Zero), Succ(x2))
new_min133(x0, x1, True)
new_min1146(x0, x1, x2, False)
new_min1106(x0, x1, x2, x3, False)
new_min1130(x0, x1, False)
new_min191(x0, False)
new_min141(x0, x1, True)
new_min193(x0, x1, x2, True)
new_min1140(x0, True)
new_min182(x0, x1, False)
new_min12(x0, x1, x2, True)
new_min112(x0, x1, True)
new_min10(x0, Pos(Zero), x1, Pos(Succ(x2)), Zero)
new_min153(x0, False)
new_min195(x0, x1, True)
new_primPlusNat1(Succ(x0), x1)
new_min1115(x0, x1, x2, True)
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x0))))
new_min1101(x0, x1, x2, False)
new_not1(x0)
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Zero)))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Zero)))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Zero)))
new_min119(x0, Neg(x1), x2, Neg(x3), Zero)
new_min182(x0, x1, True)
new_min1107(x0, x1, True)
new_min174(x0, x1, False)
new_min161(x0, x1, False)
new_min1132(x0, x1, False)
new_min1138(x0, x1, True)
new_min149(x0, x1, True)
new_min1158(x0, x1, False)
new_min1127(x0, Pos(Zero), x1, Neg(Zero), Zero)
new_min1127(x0, Neg(Zero), x1, Pos(Zero), Zero)
new_not3(Zero)
new_min138(x0, x1, False)
new_min1100(x0, x1, False)
new_min140(x0, x1, x2, True)
new_min189(x0, x1, True)
new_min1(Float(Pos(Succ(x0)), Pos(Succ(x1))), Float(Pos(Zero), Pos(Zero)))
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Pos(Zero)))
new_min1108(x0, x1, False)
new_min170(x0, x1, True)
new_min192(x0, x1, True)
new_min16(x0, x1, x2, True)
new_min161(x0, x1, True)
new_min184(x0, True)
new_min1127(x0, Neg(x1), x2, Neg(x3), Zero)
new_min1122(x0, x1, x2, False)
new_min1130(x0, x1, True)
new_min196(x0, x1, x2, x3, False)
new_min1124(x0, x1, False)
new_min158(x0, x1, x2, False)
new_min10(x0, Neg(Succ(x1)), x2, Pos(Succ(x3)), Zero)
new_min10(x0, Pos(Succ(x1)), x2, Neg(Succ(x3)), Zero)
new_min1125(x0, True)
new_min1103(x0, x1, x2, False)
new_min156(x0, x1, False)
new_not5(x0, x1)
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Neg(Succ(x1)), Neg(Succ(x2))))
new_min163(x0, x1, True)
new_min147(x0, True)
new_min132(x0, True)
new_min113(x0, x1, x2, x3, True)
new_min169(x0, x1, x2, False)
new_min10(x0, Neg(Succ(x1)), x2, Neg(Zero), Succ(x3))
new_min194(x0, True)
new_min1155(x0, x1, False)
new_min137(x0, x1, True)
new_min195(x0, x1, False)
new_not11(Zero)
new_min1(Float(Pos(Succ(x0)), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Pos(Succ(x0)), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x1))))
new_min1(Float(Neg(Succ(x0)), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Neg(Succ(x0)), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x1))))
new_min1(Float(Neg(Succ(x0)), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Succ(x0)), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x1))))
new_min1139(x0, x1, True)
new_min1151(x0, x1, True)
new_min145(x0, x1, x2, x3, True)
new_min1170(x0, x1, x2, x3, True)
new_min1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x1))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Pos(Succ(x2))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Succ(x1)), Neg(Succ(x2))))
new_min1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Neg(Succ(x1)), Pos(Succ(x2))))
new_min1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x1))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Neg(Succ(x2))))
new_min125(x0, x1, x2, True)
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Neg(Succ(x2))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Succ(x1)), Pos(Succ(x2))))
new_min1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x1))))
new_min152(x0, x1, x2, False)
new_min150(x0, x1, False)
new_not9(Zero)
new_min183(x0)
new_min1164(x0, True)
new_min10(x0, Neg(Succ(x1)), x2, Neg(Zero), Zero)
new_min198(x0, x1, x2, True)
new_min190(x0, x1, True)
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x0))))
new_min1128(x0, x1, x2, False)
new_min196(x0, x1, x2, x3, True)
new_min128(x0, x1, False)
new_min1118(x0, x1, True)
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_min142(x0, x1, x2, False)
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(x0))))
new_not0(Succ(x0), Succ(x1))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_min1110(x0, x1, x2, True)
new_min19(x0, x1, x2, x3, False)
new_min173(x0, x1, False)
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(x0))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x0))))
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x0))))
new_min1165(x0, x1, True)
new_min1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Neg(Zero), Neg(Succ(x1))))
new_min11(x0, x1, x2, x3, True)
new_min10(x0, Neg(Zero), x1, Neg(Zero), Zero)
new_min1129(x0, x1, x2, False)
new_min186(x0, True)
new_min114(x0, x1, x2, True)
new_min1108(x0, x1, True)
new_min1138(x0, x1, False)
new_min139(x0, x1, False)
new_min1136(x0, x1, True)
new_primPlusNat0(Succ(x0), Zero)
new_min1163(x0, False)
new_min168(x0, False)
new_min1(Float(Pos(Succ(x0)), x1), Float(Neg(Succ(x2)), x3))
new_min1(Float(Neg(Succ(x0)), x1), Float(Pos(Succ(x2)), x3))
new_min1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Pos(Zero), Pos(Succ(x0))), Float(Pos(Succ(x1)), Neg(Zero)))
new_min1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Pos(Succ(x0))), Float(Neg(Succ(x1)), Pos(Zero)))
new_min1(Float(Neg(Zero), Pos(Succ(x0))), Float(Pos(Succ(x1)), Pos(Zero)))
new_min1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Succ(x0))), Float(Pos(Succ(x1)), Pos(Zero)))
new_min1148(x0, x1, False)
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Zero)))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Zero)))
new_min1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Zero)))
new_not10
new_min1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Zero)))
new_min1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Zero)))
new_min162(x0, x1, True)
new_min1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x1))))
new_min1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(x1))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Pos(Succ(x1))))
new_min1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_not6(x0, x1)
new_min1127(x0, Pos(Succ(x1)), x2, Neg(Zero), Succ(x3))
new_min1127(x0, Neg(Succ(x1)), x2, Pos(Zero), Succ(x3))
new_not0(Zero, Zero)
new_min179(x0, False)
new_min1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_min1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Neg(Succ(x1))))
new_min1(Float(Neg(Zero), Neg(Succ(x0))), Float(Neg(Succ(x1)), Neg(Zero)))
new_min14(x0, x1, False)
new_min145(x0, x1, x2, x3, False)
new_min135(x0, x1, True)
new_min1104(x0, x1, True)
new_min143(x0, x1, x2, x3, True)
new_min1127(x0, Pos(x1), x2, Pos(x3), Zero)
new_min191(x0, True)
new_min112(x0, x1, False)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: